\select@language {italian}
\contentsline {chapter}{\numberline {1}Svolgimento del progetto}{5}{chapter.1}
\contentsline {section}{\numberline {1.1}Specifica del protocollo ABP}{5}{section.1.1}
\contentsline {subsection}{\numberline {1.1.1}Tre differenti casi d'implementazione}{6}{subsection.1.1.1}
\contentsline {section}{\numberline {1.2}Implementazione dell' ABP}{6}{section.1.2}
\contentsline {subsection}{\numberline {1.2.1}Implementazione standard}{6}{subsection.1.2.1}
\contentsline {subsection}{\numberline {1.2.2}Medium con possibile perdita di pacchetti}{7}{subsection.1.2.2}
\contentsline {subsubsection}{ Perdita di pacchetti solo dal lato Sender}{7}{section*.2}
\contentsline {subsubsection}{ Perdita di pacchetti solo dal lato Receiver}{8}{section*.3}
\contentsline {subsubsection}{ Perdita di pacchetti da entrambi i lati}{8}{section*.4}
\contentsline {subsection}{\numberline {1.2.3}Medium con possibile perdita e possibilit\`a di replicazione di un pacchetto}{9}{subsection.1.2.3}
\contentsline {subsubsection}{ Perdita e duplicazione solo dal lato Sender}{9}{section*.5}
\contentsline {subsubsection}{ Perdita e duplicazione solo dal lato Receiver}{10}{section*.6}
\contentsline {subsubsection}{Perdita e duplicazione da entrambi i lati}{11}{section*.7}
\contentsline {section}{\numberline {1.3}Equivalence checking}{12}{section.1.3}
\contentsline {subsection}{\numberline {1.3.1}Implementazione standard}{13}{subsection.1.3.1}
\contentsline {subsection}{\numberline {1.3.2}Perdita di pacchetti}{13}{subsection.1.3.2}
\contentsline {subsubsection}{Perdita di pacchetti solo dal lato Sender}{13}{section*.8}
\contentsline {subsubsection}{Perdita di pacchetti solo dal lato Receiver}{13}{section*.9}
\contentsline {subsubsection}{Perdita di pacchetti da entrambi i lati}{13}{section*.10}
\contentsline {subsection}{\numberline {1.3.3}Perdita e duplicazione di pacchetti}{14}{subsection.1.3.3}
\contentsline {subsubsection}{Perdita e duplicazione solo dal lato Sender}{14}{section*.11}
\contentsline {subsubsection}{Perdita e duplicazione solo dal lato Receiver}{14}{section*.12}
\contentsline {subsubsection}{Perdita e duplicazione da entrambi i lati}{14}{section*.13}
\contentsline {section}{\numberline {1.4}Formulazione di propriet\`a tramite HML}{14}{section.1.4}
\contentsline {subsection}{\numberline {1.4.1}Implementazione standard}{15}{subsection.1.4.1}
\contentsline {subsection}{\numberline {1.4.2}Perdita di pacchetti}{15}{subsection.1.4.2}
\contentsline {subsubsection}{Perdita di pacchetti solo dal lato Sender}{15}{section*.14}
\contentsline {subsubsection}{Perdita di pacchetti solo dal lato Receiver}{15}{section*.15}
\contentsline {subsubsection}{Perdita di pacchetti da entrambi i lati}{16}{section*.16}
\contentsline {subsection}{\numberline {1.4.3}Perdita e duplicazione di pacchetti}{16}{subsection.1.4.3}
\contentsline {subsubsection}{Perdita e duplicazione solo dal lato Sender}{16}{section*.17}
\contentsline {subsubsection}{Perdita e duplicazione solo dal lato Receiver}{16}{section*.18}
\contentsline {subsubsection}{Perdita e duplicazione da entrambi i lati}{17}{section*.19}
\contentsline {subsection}{\numberline {1.4.4}Controllo dei deadlock}{17}{subsection.1.4.4}
\contentsline {chapter}{\numberline {2}Conclusioni}{19}{chapter.2}
